66 XII TOPOLOGY AND TOPOLOGICAL ALGEBRA and u e x9 v e y, then p(u + v) :g p(u) + p(v) and therefore (as u + v e x + y) p(x -f y) ^p(u) +p(v). Since (2.3.11) inf (p(u) + p(v)) = p(x) + p(y), uex,vey the proof of (i) is complete. (ii) Let r be a real number > 0 and let U be the set of all x e E such that p(x) < r. Then it follows immediately from the definition (12.14.8.1) that n(U) is the set of all x e E/F such that p(x) < r. Since F is directed, the sets U, as/> runs through F and r runs through the set of real numbers >0, form a fundamental system of neighborhoods of 0 in E. Hence (ii) follows from the definition of neighborhoods in E/F (12.11). Whenever we consider E/F as a locally convex space, it is always the quotient topology that is meant, unless the contrary is expressly stated. (12.1-4.9) Every closed vector sub space of a Frechet space is a Frechet space. Every quotient of a Frechet space by a closed vector subspace is a Frechet space. The first assertion follows from above and from (3.14.5), the second from (12.14.8) and (12.11.3). Remark (12.14.10) Let E be a normed space and F a closed vector subspace of E. Then (12.14.10.1) ||x|i=inf||z||=</(0,x) Z 6 X (in the last expression, x is considered as a linear variety parallel to F in the vector space E) is a norm on E/F which defines the quotient topology, by virtue of (12.14.4), (12.14.8), and (12.11.2). Whenever we consider E/F as a normed space, it is always this norm that is meant, unless the contrary is expressly stated. More particularly, suppose that E is a Hilbert space. Then if F is a closed subspace of E, and if F' = Pp 1(G) is the orthogonal supplement of F (6.3.1), the bijective linear mapping F' -> E/F, the restriction to F' of the canonical mapping n: E->E/F, is an isometry. For by Pythagoras' theorem we have \\x' + z\\2 = \\x'\\2+ \\z\\2 for all zeF and all jc'eF; hence \\tf\\ is the infimum of the norms of elements of x' -f- F. We may therefore identify E/F with the Hilbert space F'.t it remains to prove the triangle inequality. If x, y are elements of E/F there exists a dense